set M = Maximal_wrt F;
Maximal_wrt F is (M1) by Th30;
then ex A', B' being Subset of X st
( [A',B'] >= [([#] X),([#] X)] & [A',B'] in Maximal_wrt F ) by Def19;
hence Maximal_wrt F is (C1) ; :: thesis: verum