let F1, F2 be Field of BL; :: thesis: ( A c= F1 & ( for F being Field of BL st A c= F holds

F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds

F2 c= F ) implies F1 = F2 )

assume ( A c= F1 & ( for F being Field of BL st A c= F holds

F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds

F2 c= F ) ) ; :: thesis: F1 = F2

hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def 10 :: thesis: verum

F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds

F2 c= F ) implies F1 = F2 )

assume ( A c= F1 & ( for F being Field of BL st A c= F holds

F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds

F2 c= F ) ) ; :: thesis: F1 = F2

hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def 10 :: thesis: verum