let G, H be with_finite_clique# SimpleGraph; :: thesis: ( G c= H implies clique# G <= clique# H )
assume A1: G c= H ; :: thesis: clique# G <= clique# H
consider D being finite Clique of G such that
A2: order D = clique# G by Def15;
D is Clique of H by A1, XBOOLE_1:1;
hence clique# G <= clique# H by A2, Def15; :: thesis: verum